\begin{tabbing}
ecl{-}act(${\it ds}$; ${\it da}$; $m$; $x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$ecl\_ind(\=$x$;\+
\\[0ex]$k$,${\it test}$.($\lambda$$L$.False);
\\[0ex]$a$,$b$,${\it aa}$,${\it ab}$.($\lambda$$L$.(${\it aa}$($L$))
\\[0ex]$\vee$ ($\exists$\=$L_{1}$:event{-}info(${\it ds}$;${\it da}$) List\+
\\[0ex]$\exists$\=$L_{2}$:event{-}info(${\it ds}$;${\it da}$) List\+
\\[0ex](($L$ = append($L_{1}$; $L_{2}$) $\in$ (event{-}info(${\it ds}$;${\it da}$) List))
\\[0ex]$\wedge$ (ecl{-}halt(${\it ds}$; ${\it da}$; $a$)(0,$L_{1}$))
\\[0ex]$\wedge$ (${\it ab}$($L_{2}$)))));
\-\-\\[0ex]$a$,$b$,${\it aa}$,${\it ab}$.($\lambda$$L$.((${\it aa}$($L$))
\\[0ex]$\wedge$ \=($\forall$${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List), $n$:$\mathbb{N}^{+}$.\+
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$)
\\[0ex]$\Rightarrow$ (ecl{-}halt(${\it ds}$; ${\it da}$; $b$)($n$,${\it L'}$))
\\[0ex]$\Rightarrow$ (${\it L'}$ = $L$ $\in$ (event{-}info(${\it ds}$;${\it da}$) List))))
\-\\[0ex]$\vee$ \=((${\it ab}$($L$))\+
\\[0ex]$\wedge$ \=($\forall$${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List), $n$:$\mathbb{N}^{+}$.\+
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$)
\\[0ex]$\Rightarrow$ (ecl{-}halt(${\it ds}$; ${\it da}$; $a$)($n$,${\it L'}$))
\\[0ex]$\Rightarrow$ (${\it L'}$ = $L$ $\in$ (event{-}info(${\it ds}$;${\it da}$) List)))));
\-\-\\[0ex]$a$,$b$,${\it aa}$,${\it ab}$.($\lambda$$L$.((${\it aa}$($L$))
\\[0ex]$\wedge$ \=($\forall$${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List), $n$:$\mathbb{N}$.\+
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$)
\\[0ex]$\Rightarrow$ (ecl{-}halt(${\it ds}$; ${\it da}$; $b$)($n$,${\it L'}$))
\\[0ex]$\Rightarrow$ (${\it L'}$ = $L$ $\in$ (event{-}info(${\it ds}$;${\it da}$) List))))
\-\\[0ex]$\vee$ \=((${\it ab}$($L$))\+
\\[0ex]$\wedge$ \=($\forall$${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List), $n$:$\mathbb{N}$.\+
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$)
\\[0ex]$\Rightarrow$ (ecl{-}halt(${\it ds}$; ${\it da}$; $a$)($n$,${\it L'}$))
\\[0ex]$\Rightarrow$ (${\it L'}$ = $L$ $\in$ (event{-}info(${\it ds}$;${\it da}$) List)))));
\-\-\\[0ex]$a$,${\it aa}$.star{-}append(event{-}info(${\it ds}$;${\it da}$); (ecl{-}halt(${\it ds}$; ${\it da}$; $a$)(0)); ${\it aa}$);
\\[0ex]$a$,$n$,${\it aa}$.if ($m$ =$_{0}$ $n$) then ecl{-}halt(${\it ds}$; ${\it da}$; $a$)(0) else ${\it aa}$ fi ;
\\[0ex]$a$,$n$,${\it aa}$.${\it aa}$;
\\[0ex]$a$,$l$,${\it aa}$.${\it aa}$)
\-
\end{tabbing}